r:rationals. (qpositive(r))  (r = 0  rationals)  (qpositive(-(r))) 

latex

Definitions	ff, tt, qinv(r), if b then t else f fi , qdiv(r; s), P  Q, t  T, P  Q, prop{i:l}, P  Q, qeq(r; s), P  Q, r * s, qpositive(r), P  Q, x:A. B(x), decidable(P), False, A, nequal(T; a; b), A c B, int_nzero, x:A. B(x), subtype(S; T)
Lemmas	decidable lt, assert of eq int, assert of lt int, and functionality wrt iff, assert of band, assert of bor, iff transitivity, eq int wf, lt int wf, band wf, bor wf, int nzero properties, q-elim, assert-qeq, qeq wf2, qmul wf, int inc rationals, rationals wf, qpositive wf, assert wf, or functionality wrt iff